(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
 Patrice Godefroid, SAGE (systematic dynamic test generation)
 For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
|)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun T2_31413 () (_ BitVec 16))
(declare-fun T2_31401 () (_ BitVec 16))
(declare-fun T2_31389 () (_ BitVec 16))
(declare-fun T2_31377 () (_ BitVec 16))
(declare-fun T2_31365 () (_ BitVec 16))
(declare-fun T2_31353 () (_ BitVec 16))
(declare-fun T2_31341 () (_ BitVec 16))
(declare-fun T2_31329 () (_ BitVec 16))
(declare-fun T1_31413 () (_ BitVec 8))
(declare-fun T1_31414 () (_ BitVec 8))
(declare-fun T1_31401 () (_ BitVec 8))
(declare-fun T1_31402 () (_ BitVec 8))
(declare-fun T1_31389 () (_ BitVec 8))
(declare-fun T1_31390 () (_ BitVec 8))
(declare-fun T1_31377 () (_ BitVec 8))
(declare-fun T1_31378 () (_ BitVec 8))
(declare-fun T1_31365 () (_ BitVec 8))
(declare-fun T1_31366 () (_ BitVec 8))
(declare-fun T1_31353 () (_ BitVec 8))
(declare-fun T1_31354 () (_ BitVec 8))
(declare-fun T1_31341 () (_ BitVec 8))
(declare-fun T1_31342 () (_ BitVec 8))
(declare-fun T1_31329 () (_ BitVec 8))
(declare-fun T1_31330 () (_ BitVec 8))
(assert (and true (= T2_31329 (bvor (bvshl ((_ zero_extend 8) T1_31330) (_ bv8 16)) ((_ zero_extend 8) T1_31329))) (= T2_31341 (bvor (bvshl ((_ zero_extend 8) T1_31342) (_ bv8 16)) ((_ zero_extend 8) T1_31341))) (= T2_31353 (bvor (bvshl ((_ zero_extend 8) T1_31354) (_ bv8 16)) ((_ zero_extend 8) T1_31353))) (= T2_31365 (bvor (bvshl ((_ zero_extend 8) T1_31366) (_ bv8 16)) ((_ zero_extend 8) T1_31365))) (= T2_31377 (bvor (bvshl ((_ zero_extend 8) T1_31378) (_ bv8 16)) ((_ zero_extend 8) T1_31377))) (= T2_31389 (bvor (bvshl ((_ zero_extend 8) T1_31390) (_ bv8 16)) ((_ zero_extend 8) T1_31389))) (= T2_31401 (bvor (bvshl ((_ zero_extend 8) T1_31402) (_ bv8 16)) ((_ zero_extend 8) T1_31401))) (= T2_31413 (bvor (bvshl ((_ zero_extend 8) T1_31414) (_ bv8 16)) ((_ zero_extend 8) T1_31413))) (= T2_31413 (_ bv37500 16)) (not (= T2_31329 (_ bv40965 16))) (not (= T2_31329 (_ bv34853 16))) (not (= T2_31329 (_ bv37500 16))) (not (= T2_31341 (_ bv40965 16))) (not (= T2_31341 (_ bv34853 16))) (not (= T2_31341 (_ bv37500 16))) (bvult T2_31329 T2_31341) (not (= T2_31353 (_ bv40965 16))) (not (= T2_31353 (_ bv34853 16))) (not (= T2_31353 (_ bv37500 16))) (bvult T2_31341 T2_31353) (not (= T2_31365 (_ bv40965 16))) (not (= T2_31365 (_ bv34853 16))) (not (= T2_31365 (_ bv37500 16))) (bvult T2_31353 T2_31365) (not (= T2_31377 (_ bv40965 16))) (not (= T2_31377 (_ bv34853 16))) (not (= T2_31377 (_ bv37500 16))) (bvult T2_31365 T2_31377) (not (= T2_31389 (_ bv40965 16))) (not (= T2_31389 (_ bv34853 16))) (not (= T2_31389 (_ bv37500 16))) (bvult T2_31377 T2_31389) (not (= T2_31401 (_ bv40965 16))) (not (= T2_31401 (_ bv34853 16))) (not (= T2_31401 (_ bv37500 16))) (bvult T2_31389 T2_31401) (bvult T2_31401 T2_31413)))
(check-sat)
(exit)
